Definitions | , t T, ||as||, a < b, P  Q, False, A, P & Q, A B, i j < k, , {x:A| B(x)} , {i..j }, Void, x:A B(x), x:A. B(x), (x l), #$n, r s,  x. t(x), x L. P(x), l[i], a j < b. E(j), s = t, x:A B(x), type List, Type, f(a), , <a, b>, weighted-sum(p;F), Outcome, FinProbSpace, True, P  Q, T, r * s, P   Q, x.A(x), , x:A.B(x), Top, S T, s ~ t, {T}, SQType(T), x,y:A//B(x;y) |